\begin{tabbing}
$\forall$$D$:Dsys.
\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ (\=$\forall$\=$v$:($i$:Id$\rightarrow$M($i$).state), ${\it sched}$:(Id$\rightarrow$($\mathbb{N}\rightarrow$(IdLnk+Id)+Unit)),\+\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow$M($i$).state$\rightarrow$(M($i$).da(locl($a$))+Unit)).
\-\\[0ex]d{-}comp($D$;$v$;${\it sched}$;${\it dec}$)
\\[0ex]$\in$ $t$:$\mathbb{N}\rightarrow$($\mathbb{N}$$_{\mbox{\scriptsize $<$$t$}}$$\rightarrow$($i$:Id$\rightarrow$d{-}world{-}state($D$;$i$)))$\rightarrow$($i$:Id$\rightarrow$d{-}world{-}state($D$;$i$)))
\-
\end{tabbing}